H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 1.36 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ IFR

mainModule List

((unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]) :: (a -> a -> Bool) -> [a] -> [a] -> [a])

module List where

import qualified Maybe
import qualified Prelude

deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]

deleteBy	_ _ []	=	[]
deleteBy	eq x (y : ys)	=	if x `eq` y then ys else y : deleteBy eq x ys

elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool

elem_by	_ _ []	=	False
elem_by	eq y (x : xs)	=	x `eq` y \|\| elem_by eq y xs

nubBy :: (a -> a -> Bool) -> [a] -> [a]

nubBy

eq l

nubBy' l []

where

nubBy'

[] _

[]

nubBy'

(y : ys) xs

elem_by eq y xs

nubBy' ys xs

otherwise

y : nubBy' ys (y : xs)

unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

unionBy

eq xs ys

xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

module Maybe where

import qualified List
import qualified Prelude

If Reductions:
The following If expression

if eq x y then ys else y : deleteBy eq x ys

is transformed to

deleteBy0 ys y eq x True = ys

deleteBy0 ys y eq x False = y : deleteBy eq x ys

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

mainModule List

((unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]) :: (a -> a -> Bool) -> [a] -> [a] -> [a])

module List where

import qualified Maybe
import qualified Prelude

deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]

deleteBy	_ _ []	=	[]
deleteBy	eq x (y : ys)	=	deleteBy0 ys y eq x (x `eq` y)

deleteBy0	ys y eq x True	=	ys
deleteBy0	ys y eq x False	=	y : deleteBy eq x ys

elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool

elem_by	_ _ []	=	False
elem_by	eq y (x : xs)	=	x `eq` y \|\| elem_by eq y xs

nubBy :: (a -> a -> Bool) -> [a] -> [a]

nubBy

eq l

nubBy' l []

where

nubBy'

[] _

[]

nubBy'

(y : ys) xs

elem_by eq y xs

nubBy' ys xs

otherwise

y : nubBy' ys (y : xs)

unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

unionBy

eq xs ys

xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

module Maybe where

import qualified List
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule List

((unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]) :: (a -> a -> Bool) -> [a] -> [a] -> [a])

module List where

import qualified Maybe
import qualified Prelude

deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]

deleteBy	vw vx []	=	[]
deleteBy	eq x (y : ys)	=	deleteBy0 ys y eq x (x `eq` y)

deleteBy0	ys y eq x True	=	ys
deleteBy0	ys y eq x False	=	y : deleteBy eq x ys

elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool

elem_by	vz wu []	=	False
elem_by	eq y (x : xs)	=	x `eq` y \|\| elem_by eq y xs

nubBy :: (a -> a -> Bool) -> [a] -> [a]

nubBy

eq l

nubBy' l []

where

nubBy'

[] vy

[]

nubBy'

(y : ys) xs

elem_by eq y xs

nubBy' ys xs

otherwise

y : nubBy' ys (y : xs)

unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

unionBy

eq xs ys

xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

module Maybe where

import qualified List
import qualified Prelude

Cond Reductions:
The following Function with conditions

nubBy' [] vy = []

nubBy' (y : ys) xs

| elem_by eq y xs

= nubBy' ys xs

| otherwise

= y : nubBy' ys (y : xs)

is transformed to

nubBy' [] vy = nubBy'3 [] vy

nubBy' (y : ys) xs = nubBy'2 (y : ys) xs

nubBy'1 y ys xs True = nubBy' ys xs

nubBy'1 y ys xs False = nubBy'0 y ys xs otherwise

nubBy'0 y ys xs True = y : nubBy' ys (y : xs)

nubBy'2 (y : ys) xs = nubBy'1 y ys xs (elem_by eq y xs)

nubBy'3 [] vy = []

nubBy'3 wz xu = nubBy'2 wz xu

The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

mainModule List

((unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]) :: (a -> a -> Bool) -> [a] -> [a] -> [a])

module List where

import qualified Maybe
import qualified Prelude

deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]

deleteBy	vw vx []	=	[]
deleteBy	eq x (y : ys)	=	deleteBy0 ys y eq x (x `eq` y)

deleteBy0	ys y eq x True	=	ys
deleteBy0	ys y eq x False	=	y : deleteBy eq x ys

elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool

elem_by	vz wu []	=	False
elem_by	eq y (x : xs)	=	x `eq` y \|\| elem_by eq y xs

nubBy :: (a -> a -> Bool) -> [a] -> [a]

nubBy

eq l

nubBy' l []

where

nubBy'	[] vy	=	nubBy'3 [] vy
nubBy'	(y : ys) xs	=	nubBy'2 (y : ys) xs

nubBy'0

y ys xs True

y : nubBy' ys (y : xs)

nubBy'1	y ys xs True	=	nubBy' ys xs
nubBy'1	y ys xs False	=	nubBy'0 y ys xs otherwise

nubBy'2

(y : ys) xs

nubBy'1 y ys xs (elem_by eq y xs)

nubBy'3	[] vy	=	[]
nubBy'3	wz xu	=	nubBy'2 wz xu

unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

unionBy

eq xs ys

xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

module Maybe where

import qualified List
import qualified Prelude

Let/Where Reductions:
The bindings of the following Let/Where expression

nubBy' l []

where

nubBy' [] vy = nubBy'3 [] vy

nubBy' (y : ys) xs = nubBy'2 (y : ys) xs

nubBy'0 y ys xs True = y : nubBy' ys (y : xs)

nubBy'1 y ys xs True = nubBy' ys xs

nubBy'1 y ys xs False = nubBy'0 y ys xs otherwise

nubBy'2 (y : ys) xs = nubBy'1 y ys xs (elem_by eq y xs)

nubBy'3 [] vy = []

nubBy'3 wz xu = nubBy'2 wz xu

are unpacked to the following functions on top level

nubByNubBy'3 xv [] vy = []

nubByNubBy'3 xv wz xu = nubByNubBy'2 xv wz xu

nubByNubBy'2 xv (y : ys) xs = nubByNubBy'1 xv y ys xs (elem_by xv y xs)

nubByNubBy'0 xv y ys xs True = y : nubByNubBy' xv ys (y : xs)

nubByNubBy'1 xv y ys xs True = nubByNubBy' xv ys xs

nubByNubBy'1 xv y ys xs False = nubByNubBy'0 xv y ys xs otherwise

nubByNubBy' xv [] vy = nubByNubBy'3 xv [] vy

nubByNubBy' xv (y : ys) xs = nubByNubBy'2 xv (y : ys) xs

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

mainModule List

(unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a])

module List where

import qualified Maybe
import qualified Prelude

deleteBy :: (a -> a -> Bool) -> a -> [a] -> [a]

deleteBy	vw vx []	=	[]
deleteBy	eq x (y : ys)	=	deleteBy0 ys y eq x (x `eq` y)

deleteBy0	ys y eq x True	=	ys
deleteBy0	ys y eq x False	=	y : deleteBy eq x ys

elem_by :: (a -> a -> Bool) -> a -> [a] -> Bool

elem_by	vz wu []	=	False
elem_by	eq y (x : xs)	=	x `eq` y \|\| elem_by eq y xs

nubBy :: (a -> a -> Bool) -> [a] -> [a]

nubBy

eq l

nubByNubBy' eq l []

nubByNubBy'	xv [] vy	=	nubByNubBy'3 xv [] vy
nubByNubBy'	xv (y : ys) xs	=	nubByNubBy'2 xv (y : ys) xs

nubByNubBy'0

xv y ys xs True

y : nubByNubBy' xv ys (y : xs)

nubByNubBy'1	xv y ys xs True	=	nubByNubBy' xv ys xs
nubByNubBy'1	xv y ys xs False	=	nubByNubBy'0 xv y ys xs otherwise

nubByNubBy'2

xv (y : ys) xs

nubByNubBy'1 xv y ys xs (elem_by xv y xs)

nubByNubBy'3	xv [] vy	=	[]
nubByNubBy'3	xv wz xu	=	nubByNubBy'2 xv wz xu

unionBy :: (a -> a -> Bool) -> [a] -> [a] -> [a]

unionBy

eq xs ys

xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

module Maybe where

import qualified List
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="unionBy",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="unionBy xw3",fontsize=16,color="grey",shape="box"];3 -> 4[label="",style="dashed", color="grey", weight=3];
4[label="unionBy xw3 xw4",fontsize=16,color="grey",shape="box"];4 -> 5[label="",style="dashed", color="grey", weight=3];
5[label="unionBy xw3 xw4 xw5",fontsize=16,color="black",shape="triangle"];5 -> 6[label="",style="solid", color="black", weight=3];
6 -> 168[label="",style="dashed", color="red", weight=0];
6[label="xw4 ++ foldl (flip (deleteBy xw3)) (nubBy xw3 xw5) xw4",fontsize=16,color="magenta"];6 -> 169[label="",style="dashed", color="magenta", weight=3];
6 -> 170[label="",style="dashed", color="magenta", weight=3];
169 -> 209[label="",style="dashed", color="red", weight=0];
169[label="foldl (flip (deleteBy xw3)) (nubBy xw3 xw5) xw4",fontsize=16,color="magenta"];169 -> 210[label="",style="dashed", color="magenta", weight=3];
169 -> 211[label="",style="dashed", color="magenta", weight=3];
170[label="xw4",fontsize=16,color="green",shape="box"];168[label="xw41111111 ++ xw15",fontsize=16,color="burlywood",shape="triangle"];729[label="xw41111111/xw411111110 : xw411111111",fontsize=10,color="white",style="solid",shape="box"];168 -> 729[label="",style="solid", color="burlywood", weight=9];
729 -> 188[label="",style="solid", color="burlywood", weight=3];
730[label="xw41111111/[]",fontsize=10,color="white",style="solid",shape="box"];168 -> 730[label="",style="solid", color="burlywood", weight=9];
730 -> 189[label="",style="solid", color="burlywood", weight=3];
210[label="xw4",fontsize=16,color="green",shape="box"];211[label="nubBy xw3 xw5",fontsize=16,color="black",shape="box"];211 -> 216[label="",style="solid", color="black", weight=3];
209[label="foldl (flip (deleteBy xw3)) xw18 xw411",fontsize=16,color="burlywood",shape="triangle"];731[label="xw411/xw4110 : xw4111",fontsize=10,color="white",style="solid",shape="box"];209 -> 731[label="",style="solid", color="burlywood", weight=9];
731 -> 217[label="",style="solid", color="burlywood", weight=3];
732[label="xw411/[]",fontsize=10,color="white",style="solid",shape="box"];209 -> 732[label="",style="solid", color="burlywood", weight=9];
732 -> 218[label="",style="solid", color="burlywood", weight=3];
188[label="(xw411111110 : xw411111111) ++ xw15",fontsize=16,color="black",shape="box"];188 -> 192[label="",style="solid", color="black", weight=3];
189[label="[] ++ xw15",fontsize=16,color="black",shape="box"];189 -> 193[label="",style="solid", color="black", weight=3];
216[label="nubByNubBy' xw3 xw5 []",fontsize=16,color="burlywood",shape="box"];733[label="xw5/xw50 : xw51",fontsize=10,color="white",style="solid",shape="box"];216 -> 733[label="",style="solid", color="burlywood", weight=9];
733 -> 219[label="",style="solid", color="burlywood", weight=3];
734[label="xw5/[]",fontsize=10,color="white",style="solid",shape="box"];216 -> 734[label="",style="solid", color="burlywood", weight=9];
734 -> 220[label="",style="solid", color="burlywood", weight=3];
217[label="foldl (flip (deleteBy xw3)) xw18 (xw4110 : xw4111)",fontsize=16,color="black",shape="box"];217 -> 221[label="",style="solid", color="black", weight=3];
218[label="foldl (flip (deleteBy xw3)) xw18 []",fontsize=16,color="black",shape="box"];218 -> 222[label="",style="solid", color="black", weight=3];
192[label="xw411111110 : xw411111111 ++ xw15",fontsize=16,color="green",shape="box"];192 -> 197[label="",style="dashed", color="green", weight=3];
193[label="xw15",fontsize=16,color="green",shape="box"];219[label="nubByNubBy' xw3 (xw50 : xw51) []",fontsize=16,color="black",shape="box"];219 -> 223[label="",style="solid", color="black", weight=3];
220[label="nubByNubBy' xw3 [] []",fontsize=16,color="black",shape="box"];220 -> 224[label="",style="solid", color="black", weight=3];
221 -> 209[label="",style="dashed", color="red", weight=0];
221[label="foldl (flip (deleteBy xw3)) (flip (deleteBy xw3) xw18 xw4110) xw4111",fontsize=16,color="magenta"];221 -> 225[label="",style="dashed", color="magenta", weight=3];
221 -> 226[label="",style="dashed", color="magenta", weight=3];
222[label="xw18",fontsize=16,color="green",shape="box"];197 -> 168[label="",style="dashed", color="red", weight=0];
197[label="xw411111111 ++ xw15",fontsize=16,color="magenta"];197 -> 202[label="",style="dashed", color="magenta", weight=3];
223[label="nubByNubBy'2 xw3 (xw50 : xw51) []",fontsize=16,color="black",shape="box"];223 -> 227[label="",style="solid", color="black", weight=3];
224[label="nubByNubBy'3 xw3 [] []",fontsize=16,color="black",shape="box"];224 -> 228[label="",style="solid", color="black", weight=3];
225[label="xw4111",fontsize=16,color="green",shape="box"];226[label="flip (deleteBy xw3) xw18 xw4110",fontsize=16,color="black",shape="box"];226 -> 229[label="",style="solid", color="black", weight=3];
202[label="xw411111111",fontsize=16,color="green",shape="box"];227[label="nubByNubBy'1 xw3 xw50 xw51 [] (elem_by xw3 xw50 [])",fontsize=16,color="black",shape="box"];227 -> 230[label="",style="solid", color="black", weight=3];
228[label="[]",fontsize=16,color="green",shape="box"];229[label="deleteBy xw3 xw4110 xw18",fontsize=16,color="burlywood",shape="triangle"];737[label="xw18/xw180 : xw181",fontsize=10,color="white",style="solid",shape="box"];229 -> 737[label="",style="solid", color="burlywood", weight=9];
737 -> 231[label="",style="solid", color="burlywood", weight=3];
738[label="xw18/[]",fontsize=10,color="white",style="solid",shape="box"];229 -> 738[label="",style="solid", color="burlywood", weight=9];
738 -> 232[label="",style="solid", color="burlywood", weight=3];
230[label="nubByNubBy'1 xw3 xw50 xw51 [] False",fontsize=16,color="black",shape="box"];230 -> 233[label="",style="solid", color="black", weight=3];
231[label="deleteBy xw3 xw4110 (xw180 : xw181)",fontsize=16,color="black",shape="box"];231 -> 234[label="",style="solid", color="black", weight=3];
232[label="deleteBy xw3 xw4110 []",fontsize=16,color="black",shape="box"];232 -> 235[label="",style="solid", color="black", weight=3];
233[label="nubByNubBy'0 xw3 xw50 xw51 [] otherwise",fontsize=16,color="black",shape="box"];233 -> 236[label="",style="solid", color="black", weight=3];
234 -> 237[label="",style="dashed", color="red", weight=0];
234[label="deleteBy0 xw181 xw180 xw3 xw4110 (xw3 xw4110 xw180)",fontsize=16,color="magenta"];234 -> 238[label="",style="dashed", color="magenta", weight=3];
235[label="[]",fontsize=16,color="green",shape="box"];236[label="nubByNubBy'0 xw3 xw50 xw51 [] True",fontsize=16,color="black",shape="box"];236 -> 239[label="",style="solid", color="black", weight=3];
238[label="xw3 xw4110 xw180",fontsize=16,color="green",shape="box"];238 -> 244[label="",style="dashed", color="green", weight=3];
238 -> 245[label="",style="dashed", color="green", weight=3];
237[label="deleteBy0 xw181 xw180 xw3 xw4110 xw20",fontsize=16,color="burlywood",shape="triangle"];740[label="xw20/False",fontsize=10,color="white",style="solid",shape="box"];237 -> 740[label="",style="solid", color="burlywood", weight=9];
740 -> 242[label="",style="solid", color="burlywood", weight=3];
741[label="xw20/True",fontsize=10,color="white",style="solid",shape="box"];237 -> 741[label="",style="solid", color="burlywood", weight=9];
741 -> 243[label="",style="solid", color="burlywood", weight=3];
239[label="xw50 : nubByNubBy' xw3 xw51 (xw50 : [])",fontsize=16,color="green",shape="box"];239 -> 246[label="",style="dashed", color="green", weight=3];
244[label="xw4110",fontsize=16,color="green",shape="box"];245[label="xw180",fontsize=16,color="green",shape="box"];242[label="deleteBy0 xw181 xw180 xw3 xw4110 False",fontsize=16,color="black",shape="box"];242 -> 247[label="",style="solid", color="black", weight=3];
243[label="deleteBy0 xw181 xw180 xw3 xw4110 True",fontsize=16,color="black",shape="box"];243 -> 248[label="",style="solid", color="black", weight=3];
246[label="nubByNubBy' xw3 xw51 (xw50 : [])",fontsize=16,color="burlywood",shape="triangle"];742[label="xw51/xw510 : xw511",fontsize=10,color="white",style="solid",shape="box"];246 -> 742[label="",style="solid", color="burlywood", weight=9];
742 -> 249[label="",style="solid", color="burlywood", weight=3];
743[label="xw51/[]",fontsize=10,color="white",style="solid",shape="box"];246 -> 743[label="",style="solid", color="burlywood", weight=9];
743 -> 250[label="",style="solid", color="burlywood", weight=3];
247[label="xw180 : deleteBy xw3 xw4110 xw181",fontsize=16,color="green",shape="box"];247 -> 251[label="",style="dashed", color="green", weight=3];
248[label="xw181",fontsize=16,color="green",shape="box"];249[label="nubByNubBy' xw3 (xw510 : xw511) (xw50 : [])",fontsize=16,color="black",shape="box"];249 -> 252[label="",style="solid", color="black", weight=3];
250[label="nubByNubBy' xw3 [] (xw50 : [])",fontsize=16,color="black",shape="box"];250 -> 253[label="",style="solid", color="black", weight=3];
251 -> 229[label="",style="dashed", color="red", weight=0];
251[label="deleteBy xw3 xw4110 xw181",fontsize=16,color="magenta"];251 -> 254[label="",style="dashed", color="magenta", weight=3];
252[label="nubByNubBy'2 xw3 (xw510 : xw511) (xw50 : [])",fontsize=16,color="black",shape="box"];252 -> 255[label="",style="solid", color="black", weight=3];
253[label="nubByNubBy'3 xw3 [] (xw50 : [])",fontsize=16,color="black",shape="box"];253 -> 256[label="",style="solid", color="black", weight=3];
254[label="xw181",fontsize=16,color="green",shape="box"];255[label="nubByNubBy'1 xw3 xw510 xw511 (xw50 : []) (elem_by xw3 xw510 (xw50 : []))",fontsize=16,color="black",shape="box"];255 -> 257[label="",style="solid", color="black", weight=3];
256[label="[]",fontsize=16,color="green",shape="box"];257 -> 686[label="",style="dashed", color="red", weight=0];
257[label="nubByNubBy'1 xw3 xw510 xw511 (xw50 : []) (xw3 xw50 xw510 || elem_by xw3 xw510 [])",fontsize=16,color="magenta"];257 -> 687[label="",style="dashed", color="magenta", weight=3];
257 -> 688[label="",style="dashed", color="magenta", weight=3];
257 -> 689[label="",style="dashed", color="magenta", weight=3];
257 -> 690[label="",style="dashed", color="magenta", weight=3];
257 -> 691[label="",style="dashed", color="magenta", weight=3];
257 -> 692[label="",style="dashed", color="magenta", weight=3];
257 -> 693[label="",style="dashed", color="magenta", weight=3];
687[label="xw511",fontsize=16,color="green",shape="box"];688[label="xw3",fontsize=16,color="green",shape="box"];689[label="xw50",fontsize=16,color="green",shape="box"];690[label="xw510",fontsize=16,color="green",shape="box"];691[label="[]",fontsize=16,color="green",shape="box"];692[label="xw3 xw50 xw510",fontsize=16,color="green",shape="box"];692 -> 695[label="",style="dashed", color="green", weight=3];
692 -> 696[label="",style="dashed", color="green", weight=3];
693[label="[]",fontsize=16,color="green",shape="box"];686[label="nubByNubBy'1 xw48 xw49 xw50 (xw51 : xw52) (xw55 || elem_by xw48 xw49 xw54)",fontsize=16,color="burlywood",shape="triangle"];746[label="xw55/False",fontsize=10,color="white",style="solid",shape="box"];686 -> 746[label="",style="solid", color="burlywood", weight=9];
746 -> 697[label="",style="solid", color="burlywood", weight=3];
747[label="xw55/True",fontsize=10,color="white",style="solid",shape="box"];686 -> 747[label="",style="solid", color="burlywood", weight=9];
747 -> 698[label="",style="solid", color="burlywood", weight=3];
695[label="xw50",fontsize=16,color="green",shape="box"];696[label="xw510",fontsize=16,color="green",shape="box"];697[label="nubByNubBy'1 xw48 xw49 xw50 (xw51 : xw52) (False || elem_by xw48 xw49 xw54)",fontsize=16,color="black",shape="box"];697 -> 701[label="",style="solid", color="black", weight=3];
698[label="nubByNubBy'1 xw48 xw49 xw50 (xw51 : xw52) (True || elem_by xw48 xw49 xw54)",fontsize=16,color="black",shape="box"];698 -> 702[label="",style="solid", color="black", weight=3];
701[label="nubByNubBy'1 xw48 xw49 xw50 (xw51 : xw52) (elem_by xw48 xw49 xw54)",fontsize=16,color="burlywood",shape="triangle"];748[label="xw54/xw540 : xw541",fontsize=10,color="white",style="solid",shape="box"];701 -> 748[label="",style="solid", color="burlywood", weight=9];
748 -> 703[label="",style="solid", color="burlywood", weight=3];
749[label="xw54/[]",fontsize=10,color="white",style="solid",shape="box"];701 -> 749[label="",style="solid", color="burlywood", weight=9];
749 -> 704[label="",style="solid", color="burlywood", weight=3];
702[label="nubByNubBy'1 xw48 xw49 xw50 (xw51 : xw52) True",fontsize=16,color="black",shape="box"];702 -> 705[label="",style="solid", color="black", weight=3];
703[label="nubByNubBy'1 xw48 xw49 xw50 (xw51 : xw52) (elem_by xw48 xw49 (xw540 : xw541))",fontsize=16,color="black",shape="box"];703 -> 706[label="",style="solid", color="black", weight=3];
704[label="nubByNubBy'1 xw48 xw49 xw50 (xw51 : xw52) (elem_by xw48 xw49 [])",fontsize=16,color="black",shape="box"];704 -> 707[label="",style="solid", color="black", weight=3];
705[label="nubByNubBy' xw48 xw50 (xw51 : xw52)",fontsize=16,color="burlywood",shape="triangle"];750[label="xw50/xw500 : xw501",fontsize=10,color="white",style="solid",shape="box"];705 -> 750[label="",style="solid", color="burlywood", weight=9];
750 -> 708[label="",style="solid", color="burlywood", weight=3];
751[label="xw50/[]",fontsize=10,color="white",style="solid",shape="box"];705 -> 751[label="",style="solid", color="burlywood", weight=9];
751 -> 709[label="",style="solid", color="burlywood", weight=3];
706 -> 686[label="",style="dashed", color="red", weight=0];
706[label="nubByNubBy'1 xw48 xw49 xw50 (xw51 : xw52) (xw48 xw540 xw49 || elem_by xw48 xw49 xw541)",fontsize=16,color="magenta"];706 -> 710[label="",style="dashed", color="magenta", weight=3];
706 -> 711[label="",style="dashed", color="magenta", weight=3];
707[label="nubByNubBy'1 xw48 xw49 xw50 (xw51 : xw52) False",fontsize=16,color="black",shape="box"];707 -> 712[label="",style="solid", color="black", weight=3];
708[label="nubByNubBy' xw48 (xw500 : xw501) (xw51 : xw52)",fontsize=16,color="black",shape="box"];708 -> 713[label="",style="solid", color="black", weight=3];
709[label="nubByNubBy' xw48 [] (xw51 : xw52)",fontsize=16,color="black",shape="box"];709 -> 714[label="",style="solid", color="black", weight=3];
710[label="xw541",fontsize=16,color="green",shape="box"];711[label="xw48 xw540 xw49",fontsize=16,color="green",shape="box"];711 -> 715[label="",style="dashed", color="green", weight=3];
711 -> 716[label="",style="dashed", color="green", weight=3];
712[label="nubByNubBy'0 xw48 xw49 xw50 (xw51 : xw52) otherwise",fontsize=16,color="black",shape="box"];712 -> 717[label="",style="solid", color="black", weight=3];
713[label="nubByNubBy'2 xw48 (xw500 : xw501) (xw51 : xw52)",fontsize=16,color="black",shape="box"];713 -> 718[label="",style="solid", color="black", weight=3];
714[label="nubByNubBy'3 xw48 [] (xw51 : xw52)",fontsize=16,color="black",shape="box"];714 -> 719[label="",style="solid", color="black", weight=3];
715[label="xw540",fontsize=16,color="green",shape="box"];716[label="xw49",fontsize=16,color="green",shape="box"];717[label="nubByNubBy'0 xw48 xw49 xw50 (xw51 : xw52) True",fontsize=16,color="black",shape="box"];717 -> 720[label="",style="solid", color="black", weight=3];
718 -> 701[label="",style="dashed", color="red", weight=0];
718[label="nubByNubBy'1 xw48 xw500 xw501 (xw51 : xw52) (elem_by xw48 xw500 (xw51 : xw52))",fontsize=16,color="magenta"];718 -> 721[label="",style="dashed", color="magenta", weight=3];
718 -> 722[label="",style="dashed", color="magenta", weight=3];
718 -> 723[label="",style="dashed", color="magenta", weight=3];
719[label="[]",fontsize=16,color="green",shape="box"];720[label="xw49 : nubByNubBy' xw48 xw50 (xw49 : xw51 : xw52)",fontsize=16,color="green",shape="box"];720 -> 724[label="",style="dashed", color="green", weight=3];
721[label="xw501",fontsize=16,color="green",shape="box"];722[label="xw500",fontsize=16,color="green",shape="box"];723[label="xw51 : xw52",fontsize=16,color="green",shape="box"];724 -> 705[label="",style="dashed", color="red", weight=0];
724[label="nubByNubBy' xw48 xw50 (xw49 : xw51 : xw52)",fontsize=16,color="magenta"];724 -> 725[label="",style="dashed", color="magenta", weight=3];
724 -> 726[label="",style="dashed", color="magenta", weight=3];
725[label="xw49",fontsize=16,color="green",shape="box"];726[label="xw51 : xw52",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                        ↳ DependencyGraphProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_nubByNubBy'(xw48, :(xw500, xw501), xw51, xw52, ba) → new_nubByNubBy'1(xw48, xw500, xw501, xw51, xw52, :(xw51, xw52), ba)
new_nubByNubBy'1(xw48, xw49, xw50, xw51, xw52, :(xw540, xw541), ba) → new_nubByNubBy'10(xw48, xw49, xw50, xw51, xw52, xw541, ba)
new_nubByNubBy'10(xw48, xw49, :(xw500, xw501), xw51, xw52, xw54, ba) → new_nubByNubBy'1(xw48, xw500, xw501, xw51, xw52, :(xw51, xw52), ba)
new_nubByNubBy'1(xw48, xw49, xw50, xw51, xw52, [], ba) → new_nubByNubBy'(xw48, xw50, xw49, :(xw51, xw52), ba)
new_nubByNubBy'10(xw48, xw49, xw50, xw51, xw52, :(xw540, xw541), ba) → new_nubByNubBy'10(xw48, xw49, xw50, xw51, xw52, xw541, ba)
new_nubByNubBy'10(xw48, xw49, xw50, xw51, xw52, [], ba) → new_nubByNubBy'(xw48, xw50, xw49, :(xw51, xw52), ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                        ↳ DependencyGraphProof

                          ↳ QDP

                            ↳ QDPSizeChangeProof

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_nubByNubBy'(xw48, :(xw500, xw501), xw51, xw52, ba) → new_nubByNubBy'1(xw48, xw500, xw501, xw51, xw52, :(xw51, xw52), ba)
new_nubByNubBy'1(xw48, xw49, xw50, xw51, xw52, :(xw540, xw541), ba) → new_nubByNubBy'10(xw48, xw49, xw50, xw51, xw52, xw541, ba)
new_nubByNubBy'10(xw48, xw49, :(xw500, xw501), xw51, xw52, xw54, ba) → new_nubByNubBy'1(xw48, xw500, xw501, xw51, xw52, :(xw51, xw52), ba)
new_nubByNubBy'10(xw48, xw49, xw50, xw51, xw52, :(xw540, xw541), ba) → new_nubByNubBy'10(xw48, xw49, xw50, xw51, xw52, xw541, ba)
new_nubByNubBy'10(xw48, xw49, xw50, xw51, xw52, [], ba) → new_nubByNubBy'(xw48, xw50, xw49, :(xw51, xw52), ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_nubByNubBy'10(xw48, xw49, :(xw500, xw501), xw51, xw52, xw54, ba) → new_nubByNubBy'1(xw48, xw500, xw501, xw51, xw52, :(xw51, xw52), ba)
The graph contains the following edges 1 >= 1, 3 > 2, 3 > 3, 4 >= 4, 5 >= 5, 7 >= 7
new_nubByNubBy'(xw48, :(xw500, xw501), xw51, xw52, ba) → new_nubByNubBy'1(xw48, xw500, xw501, xw51, xw52, :(xw51, xw52), ba)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 3 >= 4, 4 >= 5, 5 >= 7
new_nubByNubBy'1(xw48, xw49, xw50, xw51, xw52, :(xw540, xw541), ba) → new_nubByNubBy'10(xw48, xw49, xw50, xw51, xw52, xw541, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 >= 7
new_nubByNubBy'10(xw48, xw49, xw50, xw51, xw52, :(xw540, xw541), ba) → new_nubByNubBy'10(xw48, xw49, xw50, xw51, xw52, xw541, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4, 5 >= 5, 6 > 6, 7 >= 7
new_nubByNubBy'10(xw48, xw49, xw50, xw51, xw52, [], ba) → new_nubByNubBy'(xw48, xw50, xw49, :(xw51, xw52), ba)
The graph contains the following edges 1 >= 1, 3 >= 2, 2 >= 3, 7 >= 5

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_deleteBy0(xw181, xw180, xw3, xw4110, ba) → new_deleteBy(xw3, xw4110, xw181, ba)
new_deleteBy(xw3, xw4110, :(xw180, xw181), ba) → new_deleteBy0(xw181, xw180, xw3, xw4110, ba)

From the DPs we obtained the following set of size-change graphs:

new_deleteBy(xw3, xw4110, :(xw180, xw181), ba) → new_deleteBy0(xw181, xw180, xw3, xw4110, ba)
The graph contains the following edges 3 > 1, 3 > 2, 1 >= 3, 2 >= 4, 4 >= 5
new_deleteBy0(xw181, xw180, xw3, xw4110, ba) → new_deleteBy(xw3, xw4110, xw181, ba)
The graph contains the following edges 3 >= 1, 4 >= 2, 1 >= 3, 5 >= 4

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldl(xw3, :(xw4110, xw4111), ba) → new_foldl(xw3, xw4111, ba)

From the DPs we obtained the following set of size-change graphs:

new_foldl(xw3, :(xw4110, xw4111), ba) → new_foldl(xw3, xw4111, ba)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3

↳ HASKELL

  ↳ IFR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ LetRed

                ↳ HASKELL

                  ↳ Narrow

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                      ↳ QDP

                        ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_psPs(:(xw411111110, xw411111111), xw15, ba) → new_psPs(xw411111111, xw15, ba)

From the DPs we obtained the following set of size-change graphs:

new_psPs(:(xw411111110, xw411111111), xw15, ba) → new_psPs(xw411111111, xw15, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

deleteBy0	ys y eq x True	= ys
deleteBy0	ys y eq x False	= y : deleteBy eq x ys

nubBy'	[] vy	= nubBy'3 [] vy
nubBy'	(y : ys) xs	= nubBy'2 (y : ys) xs

nubBy'1	y ys xs True	= nubBy' ys xs
nubBy'1	y ys xs False	= nubBy'0 y ys xs otherwise

nubByNubBy'3	xv [] vy	= []
nubByNubBy'3	xv wz xu	= nubByNubBy'2 xv wz xu

nubByNubBy'1	xv y ys xs True	= nubByNubBy' xv ys xs
nubByNubBy'1	xv y ys xs False	= nubByNubBy'0 xv y ys xs otherwise

nubByNubBy'	xv [] vy	= nubByNubBy'3 xv [] vy
nubByNubBy'	xv (y : ys) xs	= nubByNubBy'2 xv (y : ys) xs